nLab locally decidable topos

Idea

Loosely speaking a locally decidable topos is a topos that is locally Boolean. Whereas in a Boolean topos every object is decidable, in a locally decidable topos every object is a quotient of a decidable object. This results in a reasonable approximation to the concept of ‘being almost Boolean’.

In Lawvere’s approach to cohesion locally decidable toposes are one of the principal classes of petit toposes (Lawvere 1991). In the 1991 paper Lawvere also hypothesizes the discrete base topos $\mathcal{S}$ that he contrasts with the cohesive topos of spaces, to be locally decidable.¹

Definition

An object $X$ in a topos $\mathcal{E}$ is called locally decidable (or, a quotient of a decidable object) iff there is an epimorphism $Y\twoheadrightarrow X$ such that $Y$ is a decidable object. $\mathcal{E}$ is called locally decidable iff every object $X$ is locally decidable.

Examples

• The classifying topos $Set[\mathbf{D}]=[FinSet_{mono},Set]$ for the theory of decidable objects $\mathbf{D}$ is locally decidable. Here $FinSet_{mono}$ is the category of finite sets and monomorphisms, whose opposite category is the carrier of the site for the so called (Myhill-) Schanuel topos.

• Every localic topos is locally decidable.

• For every Grothendieck topos $\mathcal{E}$ the full subcategory $\mathcal{E}_{QD}$ of locally decidable objects is a locally decidable topos.

Properties

• Proposition. A topos $\mathcal{E}$ is locally decidable iff there is a localic geometric morphism to a Boolean topos, or iff $\mathcal{E}$ has a site $(\mathcal{C}, J)$ with all morphisms in $\mathcal{C}$ epic.

• Locally decidable (presheaf) toposes are ‘co-étendues’ in the sense that for a small $\mathcal{C}$ the functor category $[\mathcal{C},Set]$ is locally decidable precisely if $[\mathcal{C}^{op},Set]$ is an étendue. Also the all-epic-site property is dual to the all-monic-site property of étendues. Both concepts are subsumed under the notion of having a (sub canonical) site representation with no (non-trivial) idempotents (McLarty 2006, Lawvere 2007,2008).

• A locally decidable topos has a localic geometric morphism to the Schanuel topos (cf. Johnstone 2002, p.794).

Related concepts

• Boolean topos
• petit topos
• étendue
• decidable object
• theory of decidable objects

References

• Peter Freyd, All topoi are localic - or, why permutation models prevail , JPAA 46 (1987) pp.49-58.

• Simon Henry, On toposes generated by finite cardinal objects , arxiv:1505.04987 (2015). (pdf)

• Peter Johnstone, Quotients of decidable objects in a topos , Math. Proc. Camb. Phil. Soc. 93 (1983) pp.409-419.

• Peter Johnstone, How general is a generalized space? , London Math. Soc. LNS 93 (1985) pp.77-111.

• Peter Johnstone, Sketches of an Elephant II, Oxford UP 2002. (sec. C5.4 pp.792-803)

• F. William Lawvere, Qualitative Distinctions between some Toposes of Generalized Graphs , Cont. Math. 92 (1989) pp.261-299.

• F. William Lawvere, Some Thoughts on the Future of Category Theory , pp.1-13 in Springer LNM vol. 1488 (1991).

• F. William Lawvere, Axiomatic Cohesion , TAC 19 no. 3 (2007) pp.41-49. (pdf)

• F. William Lawvere, Cohesive Toposes: Combinatorial and Infinitesimal Cases, Como Ms. 2008. (pdf)

• Colin McLarty, Every Grothendieck Topos has a One-Way Site , TAC 16 no. 5 (2006) pp.123-126. (pdf)

---

1. Lawvere uses the term ‘QD’-topos ( quotient of decidable) for ‘locally decidable topos’ in this paper. He also uses ‘SUD’-object (from separable-unramified-decidable to indicate equivalent concepts in algebra-topology-logic) for what we call a locally decidable object. In later papers Lawvere uses also the terms ‘locally separable’or ‘adequately separable’. The idea to take a locally decidable base topos is probably suggested by Galois theory where ‘locally decidable’ corresponds roughly to ‘product of separable field extensions’ for an algebra over a field $k$. This also connects the notion ‘decidable’ via Grothendieck’s Galois theory to the topological notion ‘unramified’. ↩